package no.uio.ifi.cop.prover.rete;

import java.util.LinkedList;

import no.uio.ifi.cop.common.Log;

/**
 * Stores a RETE match.
 *
 * This class is basically a LinkedList of Integers
 * with some special properties. Storing a list of I
 * Integers is all we need in order to generate the
 * cross product.
 *
 * A match in an alpha node, generates a call to its
 * belonging beta node, at which point we should do
 * the following: 
 * Generate the cross product of your 'new' match
 * and all the previous matches for that rule.
 *
 * <pre>
 * Example:
 *
 * Three beta nodes with two matches each
 *
 * p(X) = [X/a], [X/b]        (matches)
 * g(Y) = [Y/b], [Y/c]        (matches)       
 * z(U) = [U/a], [U/a]        (matches)
 *
 * then this happens.
 *
 * new fact: p(d), generates this scenario
 *
 * p(X) = [X/a], [X/b], [X/d] (matches)
 * g(Y) = [Y/b], [Y/c]        (matches)       
 * z(U) = [U/a], [U/b]        (matches)
 *
 *
 * now we have 2 * 2 * 1 = 4 new possible
 * substitutions given no variable collision,
 * namely [X/d] with the cross product of the
 * old matches in the last two beta nodes.
 *
 * Basically we would like to take the cross
 * product of the three beta nodes, but the
 * first one: p(X), should only include its newest
 * member: p(d), which is why this class has a
 * variable named 'single'. This variable
 * tells us which element inside the list which
 * is immutable, i.e., we should not loop over
 * all its possible values, but only use the
 * higest possible value for it.
 *
 * Basically this is how it works:
 *
 * p(X) = [X/a], [X/b]  gets a match
 * p(X) = [X/a], [X/b], [X/d]
 *
 * We would like to see [X/d] crossed with
 * all possible ways of matching g(Y) and z(U),
 * so we generate LinkedLists of Integers with
 * these values.
 *
 * [2, 0, 0]  == [X/d], [Y/b], [U/a]
 * [2, 1, 0]  == [X/d], [Y/c], [U/a]
 * [2, 0, 1]  == [X/d], [Y/b], [U/b]
 * [2, 1, 1]  == [X/d], [Y/b], [U/b]
 *
 *
 * which is exactly what's needed in order to
 * fetch the substitutions stored inside the
 * alpha nodes. We join substitutions to see
 * if collisions occur, if not we have a match,
 * if there is a collision there is not. In this
 * case a match on p(X) with p(d) gives us 4 new
 * ways of applying this rule since no there are
 * no collisions.
 * </pre>
 *
 *
 * @version 1.1
 * @author bjarneh@ifi.uio.no
 */


public class MatchList extends LinkedList<Integer>{

    int id; // corresponds to ReteRuleMatcher id
    int single = 0; // placement of immutable Predicate
    boolean frozen = false;
    boolean exhaused = false;
    int[] current  = null;


    public void setId(int ID){ id = ID; }

    public int getId(){ return id; }

    public void setSingle(int where){ single = where; }

    public void freeze(){
        frozen  = true;
        current = new int[super.size()];
        for(int i = 0; i < current.length; i++ ){ current[i] = 0; }
        current[single] = super.get( single );
    }

    private void freeze(int[] _clone){
        frozen  = true;
        current = _clone;
    }

    public void addFirst(Integer t){
        if(frozen){
            Log.fatal("MatchList is frozen (addFirst disabled)");
        }
        super.addFirst( t );
    }

    public void addLast(Integer t){
        if(frozen){
            Log.fatal("MatchList is frozen( addLast disabled)");
        }
        super.addLast( t );
    }


    public LinkedList<Integer> tuple(){
        LinkedList<Integer> lst = new LinkedList<Integer>();
        for( int i = 0; i < current.length; i++ ){
            lst.addLast( current[i] );
        }
        return lst;
    }

    public LinkedList<Integer> next(){
        LinkedList<Integer> lst = tuple();
        exhaused = !advance();
        return lst;
    }

    public boolean advance(){

        int max = this.size() - 1;

        for( int i = 0; i < max; i++ ){
            if( i == single ){ // untouchable
                ;
            }else if( current[i] < this.get(i) ){
                current[i]++;
                return true;
            }else{
                current[i] = 0;
            }
        }

        if( max == single){
            exhaused = true;
            return false;
        }

        if( current[max] < this.get(max) ){
            current[max]++;
            return true;
        }

        exhaused = true;
        return false;
    }

    public boolean hasNext(){
        return (! exhaused );
    }

    public MatchList clone(){
        if( ! frozen ){ Log.fatal("MatchList not frozen"); }
        MatchList cp = new MatchList();
        cp.setId( id );
        cp.setSingle( single );
        for( Integer i : this ){ cp.addLast( i ); }
        cp.freeze( current.clone() );
        return cp;
    }

    public String toString(){
        return String.format("s[%d]=%d, %s", single, this.get(single), super.toString());
    }
}
